  (in-package "ACL2")
  (include-book "../../include/src/avl-integer-keys")
  (include-book "cell")
  ;;;The AVL utils module contains methods for manipulating
  ;;;avl trees. Most of these are functions for nested
  ;;;avl trees used by the lifelike grids.


  ;;method for inserting an element into
  ;;a tree of an avl tree.
  ;; tr: the outer tree
  ;; k1: the key of the inner tree in the outer tree
  ;; k2: the desired key for the data in the inner tree.
  ;;If a tree with key "K1" doesn't exist, this method
  ;;will insert one.
  ;;Returns the new tree
  (defun nested-avl-insert (tr k1 k2 data)
    (let* ((inner-tr (cdr (avl-retrieve tr k1))))
      (if inner-tr
          (avl-insert tr k1 (avl-insert inner-tr k2 data))
          (avl-insert tr k1 (avl-insert (empty-tree) k2 data)))))

  ;;method for deleting an element of
  ;;a tree of an avl tree.
  ;; tr: the outer tree
  ;; k1: the key of the inner tree in the outer tree
  ;; k2: the desired key for the data in the inner tree.
  ;;If a tree with key "K1" doesn't exist, this method
  ;;will do nothing.
  ;;Returns the new tree.
  (defun nested-avl-delete (tr k1 k2)
    (let* ((inner-tr (cdr (avl-retrieve tr k1))))
      (if inner-tr
        (avl-insert tr k1 (avl-delete inner-tr k2))
        tr)))

  ;;Helper for nested-avl-flatten-inner-inner* 
  ;;
  ;;Accumulatively processes the elements of inner-tr-flat, putting
  ;;them into acc-lst. Returns acc-lst when finished.
  ;;See nested-avl-flatten-inner-inner* for a description of the
  ;;first two params
  (defun nested-avl-flatten-inner-inner-acc* (inner-tr-flat x acc-lst)
    (if (endp inner-tr-flat)
        acc-lst
	    (let* ((top-elem (car inner-tr-flat))
	           (top-elem-y (car top-elem))
	           (inner-tr-flat-rest (cdr inner-tr-flat)))
	         (nested-avl-flatten-inner-inner-acc* inner-tr-flat-rest
	           x (cons (cell x top-elem-y) acc-lst)))))

  ;;helper for nested-avl-flatten-inner-acc*
  ;;
  ;;inner-tr-flat: list of cons pairs whose first element is
  ;;  the desired y value, and whose second element is immaterial
  ;;x:  desired x value
  ;;
  ;;Returns a list of cells with the desired x and y values
  (defun nested-avl-flatten-inner-inner* (inner-tr-flat x)
    (nested-avl-flatten-inner-inner-acc* inner-tr-flat x nil))


  ;;helper for nested-avl-flatten-inner*
  ;;
  ;;inner-trs: list of cons pairs whose first element is the desired
  ;;  x values, and whose second element is a tree containing
  ;;  a datum at each desired y value
  ;;acc-lst: (x,y) cells accumulated from inner-trs already processed
  ;;
  ;;returns acc-lst after exhausting inner-trs
  (defun nested-avl-flatten-inner-acc* (inner-trs acc-lst)
    (if (endp inner-trs)
        acc-lst
	    (let* ((top-tr-outer (car inner-trs))
	           (top-tr-x (car top-tr-outer))
	           (top-tr (cdr top-tr-outer))
	           (top-tr-flat (avl-flatten top-tr)))
	      (nested-avl-flatten-inner-acc*
	        (cdr inner-trs)
	        (append (nested-avl-flatten-inner-inner* top-tr-flat top-tr-x)
	         acc-lst)))))

  ;;Helper for nested-avl-flatten-to-cells.
  ;;Just calls an accumulator
  (defun nested-avl-flatten-inner* (inner-trs)
    (nested-avl-flatten-inner-acc* inner-trs nil))

  ;;cells = []
  ;;flatTree = flatten(outerTree)
  ;;for (x, innerTree) in flatTree:
  ;;  flatInner = flatten(innerTree)
  ;;  for (y, t) in flatInner:
  ;;    cells.push(cell x y)
  ;;return cells
  ;;
  ;;In other words, given a two-layer avl tree,
  ;;returns a list of cells with an element for each datum
  ;;in the treee where each cell has
  ;;an x value equal to the key of its inner tree in the
  ;;outer tree, and a y value equal to its key in the inner tree
  (defun nested-avl-flatten-to-cells (tr)
    (nested-avl-flatten-inner* (avl-flatten tr)))


;;Get the cons pair for the key with the lowest
;;value in the avl tree
(defun avl-min (tr)
  (let* ((left-tr (left tr)))
    (if (empty-tree? left-tr)   
        (cons (key tr) (data tr))
        (avl-min left-tr))))

;;Get the cons pair for the key with the highest
;;value in the avl tree
(defun avl-max (tr)
  (let* ((right-tr (right tr)))
    (if (empty-tree? right-tr)  
        (cons (key tr) (data tr))
        (avl-max right-tr))))


